#include <stddef.h>
#include <stdio.h>

extern int write(int, char *, size_t);
extern int fileno(FILE *file);
extern size_t lseek(int handle, size_t offset, int whence);
extern void ro_flush_input(void);
extern int ioc_t1(void);
extern int getch(void);
extern int read(int, char *, size_t);
